Hilbert choice operator. Set up for use in theorems where
assume_xm abstraction is used outermost.
Select the correctly instantiated display form by entering the
editor alias "eps". This display form contains variable that
is bound by assume_xm.
Sequent display routine needs fixing, so that pretty choicef
display form is used when XM becomes explicit hypothesis.
